Matches in value-assignements (V): {{numOfValueMatches}}
Matches in edge-description: {{numOfDescriptionMatches}}
Rank |
Scope |
|||
-V- |
{{line.bestrank}}
|
{{line.desc}}
|
| Precondition (initial variable assignment): |
|
{{precondition}} |
| {{fault.rank}}. | {{fault.score}} | Details: | ||||
Current values:
|
||||||
1 | // Automatically generated by cegarmc |
2 | // |
3 | |
4 | |
5 | extern void __VERIFIER_assume(int); |
6 | extern int __VERIFIER_nondet_bool(); |
7 | extern char __VERIFIER_nondet_char(); |
8 | extern signed char __VERIFIER_nondet_schar(); |
9 | extern unsigned char __VERIFIER_nondet_uchar(); |
10 | extern int __VERIFIER_nondet_int(); |
11 | extern unsigned int __VERIFIER_nondet_uint(); |
12 | extern short __VERIFIER_nondet_short(); |
13 | extern unsigned short __VERIFIER_nondet_ushort(); |
14 | extern long __VERIFIER_nondet_long(); |
15 | extern unsigned long __VERIFIER_nondet_ulong(); |
16 | extern long long __VERIFIER_nondet_longlong(); |
17 | extern unsigned long long __VERIFIER_nondet_ull(); |
18 | extern float __VERIFIER_nondet_float(); |
19 | extern double __VERIFIER_nondet_double(); |
20 | extern long double __VERIFIER_nondet_longdouble(); |
21 | extern void * __VERIFIER_nondet_pointer(); |
22 | |
23 | int D_print_i; |
24 | int D_print_st; |
25 | int D_z; |
26 | int N_generate_i; |
27 | int N_generate_st; |
28 | int S1_addsub_i; |
29 | int S1_addsub_st; |
30 | int S2_presdbl_i; |
31 | int S2_presdbl_st; |
32 | int S3_zero_i; |
33 | int S3_zero_st; |
34 | int count; |
35 | int main_clk_ev; |
36 | int main_clk_neg_edge; |
37 | int main_clk_pos_edge; |
38 | int main_clk_req_up; |
39 | int main_clk_val; |
40 | int main_clk_val_t; |
41 | int main_dbl_ev; |
42 | int main_dbl_req_up; |
43 | int main_dbl_val; |
44 | int main_dbl_val_t; |
45 | int main_diff_ev; |
46 | int main_diff_req_up; |
47 | int main_diff_val; |
48 | int main_diff_val_t; |
49 | int main_in1_ev; |
50 | int main_in1_req_up; |
51 | int main_in1_val; |
52 | int main_in1_val_t; |
53 | int main_in2_ev; |
54 | int main_in2_req_up; |
55 | int main_in2_val; |
56 | int main_in2_val_t; |
57 | int main_pres_ev; |
58 | int main_pres_req_up; |
59 | int main_pres_val; |
60 | int main_pres_val_t; |
61 | int main_sum_ev; |
62 | int main_sum_req_up; |
63 | int main_sum_val; |
64 | int main_sum_val_t; |
65 | int main_zero_ev; |
66 | int main_zero_req_up; |
67 | int main_zero_val; |
68 | int main_zero_val_t; |
69 | int modFlag; |
70 | int res; |
71 | |
72 | void error(); |
73 | void N_generate(); |
74 | void S1_addsub(); |
75 | void S2_presdbl(); |
76 | void S3_zero(); |
77 | void D_print(); |
78 | void eval(); |
79 | void start_simulation(); |
80 | |
81 | |
82 | void error() { |
83 | { |
84 | goto ERROR; |
85 | ERROR: ; |
86 | return; |
87 | } |
88 | } |
89 | |
90 | void N_generate() { |
91 | auto int a; |
92 | auto int b; |
93 | { |
94 | main_in1_val_t = __VERIFIER_nondet_int(); |
95 | main_in1_req_up = 1; |
96 | main_in2_val_t = __VERIFIER_nondet_int(); |
97 | main_in2_req_up = 1; |
98 | return; |
99 | } |
100 | } |
101 | |
102 | void S1_addsub() { |
103 | auto int a; |
104 | auto int b; |
105 | { |
106 | a = main_in1_val; |
107 | b = main_in2_val; |
108 | main_sum_val_t = a + b; |
109 | main_sum_req_up = 1; |
110 | main_diff_val_t = a - b; |
111 | main_diff_req_up = 1; |
112 | return; |
113 | } |
114 | } |
115 | |
116 | void S2_presdbl() { |
117 | auto int a; |
118 | auto int b; |
119 | auto int c; |
120 | auto int d; |
121 | { |
122 | a = main_sum_val; |
123 | b = main_diff_val; |
124 | main_pres_val_t = a; |
125 | main_pres_req_up = 1; |
126 | c = a + b; |
127 | d = a - b; |
128 | main_dbl_val_t = c + d; |
129 | main_dbl_req_up = 1; |
130 | return; |
131 | } |
132 | } |
133 | |
134 | void S3_zero() { |
135 | auto int a; |
136 | auto int b; |
137 | { |
138 | a = main_pres_val; |
139 | b = main_dbl_val; |
140 | main_zero_val_t = b - (a + a); |
141 | main_zero_req_up = 1; |
142 | return; |
143 | } |
144 | } |
145 | |
146 | void D_print() { |
147 | { |
148 | D_z = main_zero_val; |
149 | return; |
150 | } |
151 | } |
152 | |
153 | void eval() { |
154 | auto int tmp; |
155 | auto int tmp___0; |
156 | auto int tmp___1; |
157 | auto int tmp___2; |
158 | auto int tmp___3; |
159 | { |
160 | { |
161 | while (1) { |
162 | { |
163 | while_0_continue: ; |
164 | if (N_generate_st == 0) { |
165 | } |
166 | else { |
167 | if (S1_addsub_st == 0) { |
168 | } |
169 | else { |
170 | if (S2_presdbl_st == 0) { |
171 | } |
172 | else { |
173 | if (S3_zero_st == 0) { |
174 | } |
175 | else { |
176 | if (D_print_st == 0) { |
177 | } |
178 | else { |
179 | goto while_0_break; |
180 | } |
181 | } |
182 | } |
183 | } |
184 | } |
185 | if (N_generate_st == 0) { |
186 | { |
187 | tmp = __VERIFIER_nondet_int(); |
188 | } |
189 | if (tmp) { |
190 | N_generate_st = 1; |
191 | N_generate(); |
192 | } |
193 | else { |
194 | } |
195 | } |
196 | else { |
197 | } |
198 | if (S1_addsub_st == 0) { |
199 | { |
200 | tmp___0 = __VERIFIER_nondet_int(); |
201 | } |
202 | if (tmp___0) { |
203 | S1_addsub_st = 1; |
204 | S1_addsub(); |
205 | } |
206 | else { |
207 | } |
208 | } |
209 | else { |
210 | } |
211 | if (S2_presdbl_st == 0) { |
212 | { |
213 | tmp___1 = __VERIFIER_nondet_int(); |
214 | } |
215 | if (tmp___1) { |
216 | S2_presdbl_st = 1; |
217 | S2_presdbl(); |
218 | } |
219 | else { |
220 | } |
221 | } |
222 | else { |
223 | } |
224 | if (S3_zero_st == 0) { |
225 | { |
226 | tmp___2 = __VERIFIER_nondet_int(); |
227 | } |
228 | if (tmp___2) { |
229 | S3_zero_st = 1; |
230 | S3_zero(); |
231 | } |
232 | else { |
233 | } |
234 | } |
235 | else { |
236 | } |
237 | if (D_print_st == 0) { |
238 | { |
239 | tmp___3 = __VERIFIER_nondet_int(); |
240 | } |
241 | if (tmp___3) { |
242 | D_print_st = 1; |
243 | D_print(); |
244 | } |
245 | else { |
246 | } |
247 | } |
248 | else { |
249 | } |
250 | } |
251 | } |
252 | while_0_break: ; |
253 | } |
254 | return; |
255 | } |
256 | } |
257 | |
258 | void start_simulation() { |
259 | auto int kernel_st; |
260 | { |
261 | kernel_st = 0; |
262 | if (main_in1_req_up == 1) { |
263 | if (main_in1_val != main_in1_val_t) { |
264 | main_in1_val = main_in1_val_t; |
265 | main_in1_ev = 0; |
266 | } |
267 | else { |
268 | } |
269 | main_in1_req_up = 0; |
270 | } |
271 | else { |
272 | } |
273 | if (main_in2_req_up == 1) { |
274 | if (main_in2_val != main_in2_val_t) { |
275 | main_in2_val = main_in2_val_t; |
276 | main_in2_ev = 0; |
277 | } |
278 | else { |
279 | } |
280 | main_in2_req_up = 0; |
281 | } |
282 | else { |
283 | } |
284 | if (main_sum_req_up == 1) { |
285 | if (main_sum_val != main_sum_val_t) { |
286 | main_sum_val = main_sum_val_t; |
287 | main_sum_ev = 0; |
288 | } |
289 | else { |
290 | } |
291 | main_sum_req_up = 0; |
292 | } |
293 | else { |
294 | } |
295 | if (main_diff_req_up == 1) { |
296 | if (main_diff_val != main_diff_val_t) { |
297 | main_diff_val = main_diff_val_t; |
298 | main_diff_ev = 0; |
299 | } |
300 | else { |
301 | } |
302 | main_diff_req_up = 0; |
303 | } |
304 | else { |
305 | } |
306 | if (main_pres_req_up == 1) { |
307 | if (main_pres_val != main_pres_val_t) { |
308 | main_pres_val = main_pres_val_t; |
309 | main_pres_ev = 0; |
310 | } |
311 | else { |
312 | } |
313 | main_pres_req_up = 0; |
314 | } |
315 | else { |
316 | } |
317 | if (main_dbl_req_up == 1) { |
318 | if (main_dbl_val != main_dbl_val_t) { |
319 | main_dbl_val = main_dbl_val_t; |
320 | main_dbl_ev = 0; |
321 | } |
322 | else { |
323 | } |
324 | main_dbl_req_up = 0; |
325 | } |
326 | else { |
327 | } |
328 | if (main_zero_req_up == 1) { |
329 | if (main_zero_val != main_zero_val_t) { |
330 | main_zero_val = main_zero_val_t; |
331 | main_zero_ev = 0; |
332 | } |
333 | else { |
334 | } |
335 | main_zero_req_up = 0; |
336 | } |
337 | else { |
338 | } |
339 | if (main_clk_req_up == 1) { |
340 | if (main_clk_val != main_clk_val_t) { |
341 | main_clk_val = main_clk_val_t; |
342 | main_clk_ev = 0; |
343 | if (main_clk_val == 1) { |
344 | main_clk_pos_edge = 0; |
345 | main_clk_neg_edge = 2; |
346 | } |
347 | else { |
348 | main_clk_neg_edge = 0; |
349 | main_clk_pos_edge = 2; |
350 | } |
351 | } |
352 | else { |
353 | } |
354 | main_clk_req_up = 0; |
355 | } |
356 | else { |
357 | } |
358 | if (N_generate_i == 1) { |
359 | N_generate_st = 0; |
360 | } |
361 | else { |
362 | N_generate_st = 2; |
363 | } |
364 | if (S1_addsub_i == 1) { |
365 | S1_addsub_st = 0; |
366 | } |
367 | else { |
368 | S1_addsub_st = 2; |
369 | } |
370 | if (S2_presdbl_i == 1) { |
371 | S2_presdbl_st = 0; |
372 | } |
373 | else { |
374 | S2_presdbl_st = 2; |
375 | } |
376 | if (S3_zero_i == 1) { |
377 | S3_zero_st = 0; |
378 | } |
379 | else { |
380 | S3_zero_st = 2; |
381 | } |
382 | if (D_print_i == 1) { |
383 | D_print_st = 0; |
384 | } |
385 | else { |
386 | D_print_st = 2; |
387 | } |
388 | if (main_in1_ev == 0) { |
389 | main_in1_ev = 1; |
390 | } |
391 | else { |
392 | } |
393 | if (main_in2_ev == 0) { |
394 | main_in2_ev = 1; |
395 | } |
396 | else { |
397 | } |
398 | if (main_sum_ev == 0) { |
399 | main_sum_ev = 1; |
400 | } |
401 | else { |
402 | } |
403 | if (main_diff_ev == 0) { |
404 | main_diff_ev = 1; |
405 | } |
406 | else { |
407 | } |
408 | if (main_pres_ev == 0) { |
409 | main_pres_ev = 1; |
410 | } |
411 | else { |
412 | } |
413 | if (main_dbl_ev == 0) { |
414 | main_dbl_ev = 1; |
415 | } |
416 | else { |
417 | } |
418 | if (main_zero_ev == 0) { |
419 | main_zero_ev = 1; |
420 | } |
421 | else { |
422 | } |
423 | if (main_clk_ev == 0) { |
424 | main_clk_ev = 1; |
425 | } |
426 | else { |
427 | } |
428 | if (main_clk_pos_edge == 0) { |
429 | main_clk_pos_edge = 1; |
430 | } |
431 | else { |
432 | } |
433 | if (main_clk_neg_edge == 0) { |
434 | main_clk_neg_edge = 1; |
435 | } |
436 | else { |
437 | } |
438 | if (main_clk_pos_edge == 1) { |
439 | N_generate_st = 0; |
440 | } |
441 | else { |
442 | } |
443 | if (main_clk_pos_edge == 1) { |
444 | S1_addsub_st = 0; |
445 | } |
446 | else { |
447 | } |
448 | if (main_clk_pos_edge == 1) { |
449 | S2_presdbl_st = 0; |
450 | } |
451 | else { |
452 | } |
453 | if (main_clk_pos_edge == 1) { |
454 | S3_zero_st = 0; |
455 | } |
456 | else { |
457 | } |
458 | if (main_clk_pos_edge == 1) { |
459 | D_print_st = 0; |
460 | } |
461 | else { |
462 | } |
463 | if (main_in1_ev == 1) { |
464 | main_in1_ev = 2; |
465 | } |
466 | else { |
467 | } |
468 | if (main_in2_ev == 1) { |
469 | main_in2_ev = 2; |
470 | } |
471 | else { |
472 | } |
473 | if (main_sum_ev == 1) { |
474 | main_sum_ev = 2; |
475 | } |
476 | else { |
477 | } |
478 | if (main_diff_ev == 1) { |
479 | main_diff_ev = 2; |
480 | } |
481 | else { |
482 | } |
483 | if (main_pres_ev == 1) { |
484 | main_pres_ev = 2; |
485 | } |
486 | else { |
487 | } |
488 | if (main_dbl_ev == 1) { |
489 | main_dbl_ev = 2; |
490 | } |
491 | else { |
492 | } |
493 | if (main_zero_ev == 1) { |
494 | main_zero_ev = 2; |
495 | } |
496 | else { |
497 | } |
498 | if (main_clk_ev == 1) { |
499 | main_clk_ev = 2; |
500 | } |
501 | else { |
502 | } |
503 | if (main_clk_pos_edge == 1) { |
504 | main_clk_pos_edge = 2; |
505 | } |
506 | else { |
507 | } |
508 | if (main_clk_neg_edge == 1) { |
509 | main_clk_neg_edge = 2; |
510 | } |
511 | else { |
512 | } |
513 | { |
514 | while (1) { |
515 | { |
516 | while_1_continue: ; |
517 | { |
518 | kernel_st = 1; |
519 | eval(); |
520 | } |
521 | kernel_st = 2; |
522 | if (main_in1_req_up == 1) { |
523 | if (main_in1_val != main_in1_val_t) { |
524 | main_in1_val = main_in1_val_t; |
525 | main_in1_ev = 0; |
526 | } |
527 | else { |
528 | } |
529 | main_in1_req_up = 0; |
530 | } |
531 | else { |
532 | } |
533 | if (main_in2_req_up == 1) { |
534 | if (main_in2_val != main_in2_val_t) { |
535 | main_in2_val = main_in2_val_t; |
536 | main_in2_ev = 0; |
537 | } |
538 | else { |
539 | } |
540 | main_in2_req_up = 0; |
541 | } |
542 | else { |
543 | } |
544 | if (main_sum_req_up == 1) { |
545 | if (main_sum_val != main_sum_val_t) { |
546 | main_sum_val = main_sum_val_t; |
547 | main_sum_ev = 0; |
548 | } |
549 | else { |
550 | } |
551 | main_sum_req_up = 0; |
552 | } |
553 | else { |
554 | } |
555 | if (main_diff_req_up == 1) { |
556 | if (main_diff_val != main_diff_val_t) { |
557 | main_diff_val = main_diff_val_t; |
558 | main_diff_ev = 0; |
559 | } |
560 | else { |
561 | } |
562 | main_diff_req_up = 0; |
563 | } |
564 | else { |
565 | } |
566 | if (main_pres_req_up == 1) { |
567 | if (main_pres_val != main_pres_val_t) { |
568 | main_pres_val = main_pres_val_t; |
569 | main_pres_ev = 0; |
570 | } |
571 | else { |
572 | } |
573 | main_pres_req_up = 0; |
574 | } |
575 | else { |
576 | } |
577 | if (main_dbl_req_up == 1) { |
578 | if (main_dbl_val != main_dbl_val_t) { |
579 | main_dbl_val = main_dbl_val_t; |
580 | main_dbl_ev = 0; |
581 | } |
582 | else { |
583 | } |
584 | main_dbl_req_up = 0; |
585 | } |
586 | else { |
587 | } |
588 | if (main_zero_req_up == 1) { |
589 | if (main_zero_val != main_zero_val_t) { |
590 | main_zero_val = main_zero_val_t; |
591 | main_zero_ev = 0; |
592 | } |
593 | else { |
594 | } |
595 | main_zero_req_up = 0; |
596 | } |
597 | else { |
598 | } |
599 | if (main_clk_req_up == 1) { |
600 | if (main_clk_val != main_clk_val_t) { |
601 | main_clk_val = main_clk_val_t; |
602 | main_clk_ev = 0; |
603 | if (main_clk_val == 1) { |
604 | main_clk_pos_edge = 0; |
605 | main_clk_neg_edge = 2; |
606 | } |
607 | else { |
608 | main_clk_neg_edge = 0; |
609 | main_clk_pos_edge = 2; |
610 | } |
611 | } |
612 | else { |
613 | } |
614 | main_clk_req_up = 0; |
615 | } |
616 | else { |
617 | } |
618 | kernel_st = 3; |
619 | if (main_in1_ev == 0) { |
620 | main_in1_ev = 1; |
621 | } |
622 | else { |
623 | } |
624 | if (main_in2_ev == 0) { |
625 | main_in2_ev = 1; |
626 | } |
627 | else { |
628 | } |
629 | if (main_sum_ev == 0) { |
630 | main_sum_ev = 1; |
631 | } |
632 | else { |
633 | } |
634 | if (main_diff_ev == 0) { |
635 | main_diff_ev = 1; |
636 | } |
637 | else { |
638 | } |
639 | if (main_pres_ev == 0) { |
640 | main_pres_ev = 1; |
641 | } |
642 | else { |
643 | } |
644 | if (main_dbl_ev == 0) { |
645 | main_dbl_ev = 1; |
646 | } |
647 | else { |
648 | } |
649 | if (main_zero_ev == 0) { |
650 | main_zero_ev = 1; |
651 | } |
652 | else { |
653 | } |
654 | if (main_clk_ev == 0) { |
655 | main_clk_ev = 1; |
656 | } |
657 | else { |
658 | } |
659 | if (main_clk_pos_edge == 0) { |
660 | main_clk_pos_edge = 1; |
661 | } |
662 | else { |
663 | } |
664 | if (main_clk_neg_edge == 0) { |
665 | main_clk_neg_edge = 1; |
666 | } |
667 | else { |
668 | } |
669 | if (main_clk_pos_edge == 1) { |
670 | N_generate_st = 0; |
671 | } |
672 | else { |
673 | } |
674 | if (main_clk_pos_edge == 1) { |
675 | S1_addsub_st = 0; |
676 | } |
677 | else { |
678 | } |
679 | if (main_clk_pos_edge == 1) { |
680 | S2_presdbl_st = 0; |
681 | } |
682 | else { |
683 | } |
684 | if (main_clk_pos_edge == 1) { |
685 | S3_zero_st = 0; |
686 | } |
687 | else { |
688 | } |
689 | if (main_clk_pos_edge == 1) { |
690 | D_print_st = 0; |
691 | } |
692 | else { |
693 | } |
694 | if (main_in1_ev == 1) { |
695 | main_in1_ev = 2; |
696 | } |
697 | else { |
698 | } |
699 | if (main_in2_ev == 1) { |
700 | main_in2_ev = 2; |
701 | } |
702 | else { |
703 | } |
704 | if (main_sum_ev == 1) { |
705 | main_sum_ev = 2; |
706 | } |
707 | else { |
708 | } |
709 | if (main_diff_ev == 1) { |
710 | main_diff_ev = 2; |
711 | } |
712 | else { |
713 | } |
714 | if (main_pres_ev == 1) { |
715 | main_pres_ev = 2; |
716 | } |
717 | else { |
718 | } |
719 | if (main_dbl_ev == 1) { |
720 | main_dbl_ev = 2; |
721 | } |
722 | else { |
723 | } |
724 | if (main_zero_ev == 1) { |
725 | main_zero_ev = 2; |
726 | } |
727 | else { |
728 | } |
729 | if (main_clk_ev == 1) { |
730 | main_clk_ev = 2; |
731 | } |
732 | else { |
733 | } |
734 | if (main_clk_pos_edge == 1) { |
735 | main_clk_pos_edge = 2; |
736 | } |
737 | else { |
738 | } |
739 | if (main_clk_neg_edge == 1) { |
740 | main_clk_neg_edge = 2; |
741 | } |
742 | else { |
743 | } |
744 | if (N_generate_st == 0) { |
745 | } |
746 | else { |
747 | if (S1_addsub_st == 0) { |
748 | } |
749 | else { |
750 | if (S2_presdbl_st == 0) { |
751 | } |
752 | else { |
753 | if (S3_zero_st == 0) { |
754 | } |
755 | else { |
756 | if (D_print_st == 0) { |
757 | } |
758 | else { |
759 | goto while_1_break; |
760 | } |
761 | } |
762 | } |
763 | } |
764 | } |
765 | } |
766 | } |
767 | while_1_break: ; |
768 | } |
769 | return; |
770 | } |
771 | } |
772 | |
773 | void main () { |
774 | // |
775 | // Number of lvals: 62 |
776 | // Frama_C_interval: int (int min, int max) |
777 | // int (int min, int max) |
778 | // error: void (void) |
779 | // void (void) |
780 | // count: int |
781 | // int |
782 | // res: int |
783 | // int |
784 | // modFlag: int |
785 | // int |
786 | // main_in1_val: int |
787 | // int |
788 | // main_in1_val_t: int |
789 | // int |
790 | // main_in1_ev: int |
791 | // int |
792 | // main_in1_req_up: int |
793 | // int |
794 | // main_in2_val: int |
795 | // int |
796 | // main_in2_val_t: int |
797 | // int |
798 | // main_in2_ev: int |
799 | // int |
800 | // main_in2_req_up: int |
801 | // int |
802 | // main_diff_val: int |
803 | // int |
804 | // main_diff_val_t: int |
805 | // int |
806 | // main_diff_ev: int |
807 | // int |
808 | // main_diff_req_up: int |
809 | // int |
810 | // main_sum_val: int |
811 | // int |
812 | // main_sum_val_t: int |
813 | // int |
814 | // main_sum_ev: int |
815 | // int |
816 | // main_sum_req_up: int |
817 | // int |
818 | // main_pres_val: int |
819 | // int |
820 | // main_pres_val_t: int |
821 | // int |
822 | // main_pres_ev: int |
823 | // int |
824 | // main_pres_req_up: int |
825 | // int |
826 | // main_dbl_val: int |
827 | // int |
828 | // main_dbl_val_t: int |
829 | // int |
830 | // main_dbl_ev: int |
831 | // int |
832 | // main_dbl_req_up: int |
833 | // int |
834 | // main_zero_val: int |
835 | // int |
836 | // main_zero_val_t: int |
837 | // int |
838 | // main_zero_ev: int |
839 | // int |
840 | // main_zero_req_up: int |
841 | // int |
842 | // main_clk_val: int |
843 | // int |
844 | // main_clk_val_t: int |
845 | // int |
846 | // main_clk_ev: int |
847 | // int |
848 | // main_clk_req_up: int |
849 | // int |
850 | // main_clk_pos_edge: int |
851 | // int |
852 | // main_clk_neg_edge: int |
853 | // int |
854 | // N_generate_st: int |
855 | // int |
856 | // N_generate_i: int |
857 | // int |
858 | // S1_addsub_st: int |
859 | // int |
860 | // S1_addsub_i: int |
861 | // int |
862 | // S2_presdbl_st: int |
863 | // int |
864 | // S2_presdbl_i: int |
865 | // int |
866 | // S3_zero_st: int |
867 | // int |
868 | // S3_zero_i: int |
869 | // int |
870 | // D_z: int |
871 | // int |
872 | // D_print_st: int |
873 | // int |
874 | // D_print_i: int |
875 | // int |
876 | // N_generate: void (void) |
877 | // void (void) |
878 | // S1_addsub: void (void) |
879 | // void (void) |
880 | // S2_presdbl: void (void) |
881 | // void (void) |
882 | // S3_zero: void (void) |
883 | // void (void) |
884 | // D_print: void (void) |
885 | // void (void) |
886 | // eval: void (void) |
887 | // void (void) |
888 | // start_simulation: void (void) |
889 | // void (void) |
890 | // n1: int |
891 | // int |
892 | // n2: int |
893 | // int |
894 | // n3: int |
895 | // int |
896 | // bound: int |
897 | // int |
898 | // i: int |
899 | // int |
900 | // |
901 | |
902 | D_print_i = __VERIFIER_nondet_int(); |
903 | D_print_st = __VERIFIER_nondet_int(); |
904 | D_z = __VERIFIER_nondet_int(); |
905 | N_generate_i = __VERIFIER_nondet_int(); |
906 | N_generate_st = __VERIFIER_nondet_int(); |
907 | S1_addsub_i = __VERIFIER_nondet_int(); |
908 | S1_addsub_st = __VERIFIER_nondet_int(); |
909 | S2_presdbl_i = __VERIFIER_nondet_int(); |
910 | S2_presdbl_st = __VERIFIER_nondet_int(); |
911 | S3_zero_i = __VERIFIER_nondet_int(); |
912 | S3_zero_st = __VERIFIER_nondet_int(); |
913 | count = __VERIFIER_nondet_int(); |
914 | main_clk_ev = __VERIFIER_nondet_int(); |
915 | main_clk_neg_edge = __VERIFIER_nondet_int(); |
916 | main_clk_pos_edge = __VERIFIER_nondet_int(); |
917 | main_clk_req_up = __VERIFIER_nondet_int(); |
918 | main_clk_val = __VERIFIER_nondet_int(); |
919 | main_clk_val_t = __VERIFIER_nondet_int(); |
920 | main_dbl_ev = __VERIFIER_nondet_int(); |
921 | main_dbl_req_up = __VERIFIER_nondet_int(); |
922 | main_dbl_val = __VERIFIER_nondet_int(); |
923 | main_dbl_val_t = __VERIFIER_nondet_int(); |
924 | main_diff_ev = __VERIFIER_nondet_int(); |
925 | main_diff_req_up = __VERIFIER_nondet_int(); |
926 | main_diff_val = __VERIFIER_nondet_int(); |
927 | main_diff_val_t = __VERIFIER_nondet_int(); |
928 | main_in1_ev = __VERIFIER_nondet_int(); |
929 | main_in1_req_up = __VERIFIER_nondet_int(); |
930 | main_in1_val = __VERIFIER_nondet_int(); |
931 | main_in1_val_t = __VERIFIER_nondet_int(); |
932 | main_in2_ev = __VERIFIER_nondet_int(); |
933 | main_in2_req_up = __VERIFIER_nondet_int(); |
934 | main_in2_val = __VERIFIER_nondet_int(); |
935 | main_in2_val_t = __VERIFIER_nondet_int(); |
936 | main_pres_ev = __VERIFIER_nondet_int(); |
937 | main_pres_req_up = __VERIFIER_nondet_int(); |
938 | main_pres_val = __VERIFIER_nondet_int(); |
939 | main_pres_val_t = __VERIFIER_nondet_int(); |
940 | main_sum_ev = __VERIFIER_nondet_int(); |
941 | main_sum_req_up = __VERIFIER_nondet_int(); |
942 | main_sum_val = __VERIFIER_nondet_int(); |
943 | main_sum_val_t = __VERIFIER_nondet_int(); |
944 | main_zero_ev = __VERIFIER_nondet_int(); |
945 | main_zero_req_up = __VERIFIER_nondet_int(); |
946 | main_zero_val = __VERIFIER_nondet_int(); |
947 | main_zero_val_t = __VERIFIER_nondet_int(); |
948 | modFlag = __VERIFIER_nondet_int(); |
949 | res = __VERIFIER_nondet_int(); |
950 | |
951 | |
952 | |
953 | { |
954 | int n1 = 3; |
955 | int n2 = 5; |
956 | int n3 = 7; |
957 | res = 0; |
958 | auto int bound; |
959 | bound = __VERIFIER_nondet_int(); |
960 | { |
961 | int i = 0; |
962 | while (1) { |
963 | if (i < bound) { |
964 | } |
965 | else { |
966 | break; |
967 | } |
968 | { |
969 | if (i % n1 == 0) { |
970 | if (i % n2 == 0) { |
971 | if (i % n3 == 0) { |
972 | res = i; |
973 | } |
974 | else { |
975 | } |
976 | } |
977 | else { |
978 | } |
979 | } |
980 | else { |
981 | } |
982 | } |
983 | i ++; |
984 | } |
985 | } |
986 | { |
987 | modFlag = res; |
988 | } |
989 | if (modFlag % 105 == 0) { |
990 | { |
991 | count = 0; |
992 | main_in1_ev = 2; |
993 | main_in1_req_up = 0; |
994 | main_in2_ev = 2; |
995 | main_in2_req_up = 0; |
996 | main_diff_ev = 2; |
997 | main_diff_req_up = 0; |
998 | main_sum_ev = 2; |
999 | main_sum_req_up = 0; |
1000 | main_pres_ev = 2; |
1001 | main_pres_req_up = 0; |
1002 | main_dbl_ev = 2; |
1003 | main_dbl_req_up = 0; |
1004 | main_zero_ev = 2; |
1005 | main_zero_req_up = 0; |
1006 | main_clk_val = 0; |
1007 | main_clk_ev = 2; |
1008 | main_clk_req_up = 0; |
1009 | main_clk_pos_edge = 2; |
1010 | main_clk_neg_edge = 2; |
1011 | count = 0; |
1012 | N_generate_i = 0; |
1013 | S1_addsub_i = 0; |
1014 | S2_presdbl_i = 0; |
1015 | S3_zero_i = 0; |
1016 | D_print_i = 0; |
1017 | start_simulation(); |
1018 | } |
1019 | { |
1020 | while (1) { |
1021 | { |
1022 | while_2_continue: ; |
1023 | { |
1024 | main_clk_val_t = 1; |
1025 | main_clk_req_up = 1; |
1026 | start_simulation(); |
1027 | count ++; |
1028 | } |
1029 | if (count == 5) { |
1030 | if (! (D_z == 0)) { |
1031 | error(); |
1032 | } |
1033 | else { |
1034 | } |
1035 | count = 0; |
1036 | } |
1037 | else { |
1038 | } |
1039 | { |
1040 | main_clk_val_t = 0; |
1041 | main_clk_req_up = 1; |
1042 | start_simulation(); |
1043 | } |
1044 | } |
1045 | } |
1046 | } |
1047 | } |
1048 | else { |
1049 | error(); |
1050 | } |
1051 | } |
1052 | return; |
1053 | } |
| Date | Time | Level | Component | Message |
|---|---|---|---|---|
| 2023-06-28 | 04:19:09:396 | INFO | CPAMain.detectFrontendLanguageIfNecessary | Language C detected and set for analysis |
| 2023-06-28 | 04:19:09:413 | INFO | ResourceLimitChecker.fromConfiguration | Using the following resource limits: CPU-time limit of 900s |
| 2023-06-28 | 04:19:09:467 | INFO | CPAchecker.run | CPAchecker 2.2 / svcomp23 (OpenJDK 64-Bit Server VM 11.0.19) started |
| 2023-06-28 | 04:19:09:484 | INFO | CPAchecker.parse | Parsing CFA from file(s) "no_context/combo2.c" |
| 2023-06-28 | 04:19:10:457 | INFO | CoreComponentsFactory.createAlgorithm | Using heuristics to select analysis |
| 2023-06-28 | 04:19:10:469 | WARNING | CPAchecker.printConfigurationWarnings | The following configuration options were specified but are not used: cpa.callstack.unsupportedFunctions termination.violation.witness cpa.predicate.memoryAllocationsAlwaysSucceed cpa.arg.compressWitness cpa.callstack.skipFunctionPointerRecursion cpa.composite.aggregateBasicBlocks counterexample.export.graphml counterexample.export.compressWitness cpa.arg.proofWitness |
| 2023-06-28 | 04:19:10:469 | INFO | CPAchecker.runAlgorithm | Starting analysis ... |
| 2023-06-28 | 04:19:10:473 | INFO | SelectionAlgorithm.chooseConfig | Performing heuristic ... |
| 2023-06-28 | 04:19:10:477 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties ResourceLimitChecker.fromConfiguration | Using the following resource limits: CPU-time limit of 900s |
| 2023-06-28 | 04:19:10:502 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties CoreComponentsFactory.createAlgorithm | Using Restarting Algorithm |
| 2023-06-28 | 04:19:10:508 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties RestartAlgorithm.run | Loading analysis 1 from file /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties ... |
| 2023-06-28 | 04:19:10:513 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties NestingAlgorithm.checkConfigs | Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties': 'cpa.composite.aggregateBasicBlocks' has two values 'false' and 'true'. Using 'true'. |
| 2023-06-28 | 04:19:10:513 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties NestingAlgorithm.checkConfigs | Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties': 'limits.time.cpu' has two values '900s' and '140s'. Using '140s'. |
| 2023-06-28 | 04:19:10:513 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties NestingAlgorithm.checkConfigs | Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties': 'limits.time.cpu::required' has two values '900' and '140s'. Using '140s'. |
| 2023-06-28 | 04:19:10:514 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties ResourceLimitChecker.fromConfiguration | Using the following resource limits: CPU-time limit of 140s |
| 2023-06-28 | 04:19:10:809 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties RestartAlgorithm.run | Starting analysis 1 ... |
| 2023-06-28 | 04:21:12:614 | WARNING | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties ShutdownNotifier.shutdownIfNecessary | Warning: Analysis 1 stopped. (The CPU-time limit of 140s has elapsed.) |
| 2023-06-28 | 04:21:12:956 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties RestartAlgorithm.run | RestartAlgorithm switches to the next configuration... |
| 2023-06-28 | 04:21:12:957 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties RestartAlgorithm.run | Loading analysis 2 from file /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties ... |
| 2023-06-28 | 04:21:12:960 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties NestingAlgorithm.checkConfigs | Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties': 'cpa.composite.aggregateBasicBlocks' has two values 'false' and 'true'. Using 'true'. |
| 2023-06-28 | 04:21:12:960 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties NestingAlgorithm.checkConfigs | Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties': 'limits.time.cpu' has two values '900s' and '60s'. Using '60s'. |
| 2023-06-28 | 04:21:12:961 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties NestingAlgorithm.checkConfigs | Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties': 'limits.time.cpu::required' has two values '900' and '60s'. Using '60s'. |
| 2023-06-28 | 04:21:12:961 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties ResourceLimitChecker.fromConfiguration | Using the following resource limits: CPU-time limit of 60s |
| 2023-06-28 | 04:21:13:014 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties RestartAlgorithm.run | Starting analysis 2 ... |
| 2023-06-28 | 04:21:13:104 | INFO | CPAchecker.runAlgorithm | Stopping analysis ... |
| Statistics Name | Statistics Value | Additional Value |
|---|---|---|
| Selection Algorithm statistics | ||
| Size of preliminary analysis reached set | 0 | |
| Used algorithm property | /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties | |
| Program containing only relevant bools | 0 | |
| Relevant boolean vars / relevant vars ratio | 0.0676 | |
| Requires alias handling | 0 | |
| Requires loop handling | 1 | |
| Has a single loop | 0 | |
| Requires composite-type handling | 0 | |
| Requires array handling | 0 | |
| Requires float handling | 0 | |
| Requires recursion handling | 0 | |
| Relevant addressed vars / relevant vars ratio | 0.0000 | |
| Program containing external functions | true | |
| Number of all righthand side functions | 9 | |
| Restart Algorithm statistics | ||
| Number of algorithms provided | 7 | |
| Number of algorithms used | 2 | |
| Total time for algorithm 2 | 0.147s | |
| ValueAnalysisCPA statistics | ||
| Number of variables per state | 0.00 | sum: 0, count: 1448, min: 0, max: 0 |
| Number of global variables per state | 0.00 | sum: 0, count: 1448, min: 0, max: 0 |
| Number of assumptions | 668 | |
| Number of deterministic assumptions | 0 | |
| Level of Determinism | 0% | |
| ValueAnalysisPrecisionAdjustment statistics | ||
| Number of abstraction computations | 1781 | |
| Total time for liveness abstraction | 0.000s | |
| Total time for abstraction computation | 0.007s | |
| Total time for path thresholds | 0.000s | |
| ConstraintsStrengthenOperator statistics | ||
| Total time for strengthening by ConstraintsCPA | 0.000s | |
| Replaced symbolic expressions | 0 | |
| AutomatonAnalysis (SVCOMP) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.001s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 2122, count: 2122, min: 1, max: 1 [1 x 2122] |
| Number of states with assumption transitions | 0 | |
| CPA algorithm statistics | ||
| Number of iterations | 1448 | |
| Max size of waitlist | 27 | |
| Average size of waitlist | 13 | |
| Number of computed successors | 1781 | |
| Max successors for one state | 2 | |
| Number of times merged | 0 | |
| Number of times stopped | 334 | |
| Number of times breaked | 0 | |
| Total time for CPA algorithm | 0.079s | Max: 0.079s |
| Time for choose from waitlist | 0.012s | |
| Time for precision adjustment | 0.014s | |
| Time for transfer relation | 0.029s | |
| Time for stop operator | 0.004s | |
| Time for adding to reached set | 0.010s | |
| ValueAnalysisRefiner statistics | ||
| Number of refinements | 0 | |
| Number of targets found | 0 | count: 0, min: 0, max: 0, avg: 0.00 |
| Time for completing refinement | 0.000s | |
| Number of root relocations | 0 | |
| Number of similar, repeated refinements | 0 | |
| Number of unique precision increments | 0 | |
| PathExtractor statistics | ||
| Total number of targets found | 0 | |
| ValueAnalysisPathInterpolator statistics | ||
| Time for interpolation | 0.000s | |
| Number of interpolations | 0 | |
| Number of interpolation queries | 0 | count: 0, min: 0, max: 0, avg: 0.00 |
| Size of interpolant | 0.00 | sum: 0, count: 0, min: 0, max: 0 |
| Number of sliced prefixes | 0 | count: 0, min: 0, max: 0, avg: 0.00 |
| Extracting infeasible sliced prefixes | 0.000s | |
| Selecting infeasible sliced prefixes | 0.000s | |
| CEGAR algorithm statistics | ||
| Number of CEGAR refinements | 0 | |
| Counterexample-Check Algorithm statistics | ||
| Number of counterexample checks | 0 | |
| CPA algorithm statistics | ||
| Number of iterations | 1448 | |
| Max size of waitlist | 27 | |
| Average size of waitlist | 13 | |
| Number of computed successors | 1781 | |
| Max successors for one state | 2 | |
| Number of times merged | 0 | |
| Number of times stopped | 334 | |
| Number of times breaked | 0 | |
| Total time for CPA algorithm | 0.079s | Max: 0.079s |
| Time for choose from waitlist | 0.012s | |
| Time for precision adjustment | 0.014s | |
| Time for transfer relation | 0.029s | |
| Time for stop operator | 0.004s | |
| Time for adding to reached set | 0.010s | |
| ValueAnalysisRefiner statistics | ||
| Number of refinements | 0 | |
| Number of targets found | 0 | count: 0, min: 0, max: 0, avg: 0.00 |
| Time for completing refinement | 0.000s | |
| Number of root relocations | 0 | |
| Number of similar, repeated refinements | 0 | |
| Number of unique precision increments | 0 | |
| PathExtractor statistics | ||
| Total number of targets found | 0 | |
| ValueAnalysisPathInterpolator statistics | ||
| Time for interpolation | 0.000s | |
| Number of interpolations | 0 | |
| Number of interpolation queries | 0 | count: 0, min: 0, max: 0, avg: 0.00 |
| Size of interpolant | 0.00 | sum: 0, count: 0, min: 0, max: 0 |
| Number of sliced prefixes | 0 | count: 0, min: 0, max: 0, avg: 0.00 |
| Extracting infeasible sliced prefixes | 0.000s | |
| Selecting infeasible sliced prefixes | 0.000s | |
| CEGAR algorithm statistics | ||
| Number of CEGAR refinements | 0 | |
| Counterexample-Check Algorithm statistics | ||
| Number of counterexample checks | 0 | |
| Code Coverage | ||
| Function coverage | 1.000 | |
| Visited lines | 457 | |
| Total lines | 457 | |
| Line coverage | 1.000 | |
| Visited conditions | 232 | |
| Total conditions | 232 | |
| Condition coverage | 1.000 | |
| CPAchecker general statistics | ||
| Number of program locations | 734 | |
| Number of CFA edges (per node) | 863 | count: 734, min: 0, max: 3, avg: 1.18 |
| Number of relevant variables | 74 | |
| Number of functions | 9 | |
| Number of loops (and loop nodes) | 4 | sum: 291, min: 17, max: 196, avg: 72.75 |
| Size of reached set | 1448 | |
| Number of reached locations | 513 | 70% |
| Avg states per location | 2 | |
| Max states per location | 3 | at node N7 |
| Number of reached functions | 9 | 100% |
| Number of target states | 0 | |
| Time for analysis setup | 0.985s | |
| Time for loading CPAs | 0.134s | |
| Time for loading parser | 0.146s | |
| Time for CFA construction | 0.678s | |
| Time for parsing file(s) | 0.258s | |
| Time for AST to CFA | 0.160s | |
| Time for CFA sanity check | 0.046s | |
| Time for post-processing | 0.150s | |
| Time for CFA export | 0.849s | |
| Time for function pointers resolving | 0.005s | |
| Function calls via function pointers | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Instrumented function pointer calls | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Function calls with function pointer arguments | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Instrumented function pointer arguments | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Time for classifying variables | 0.086s | |
| Time for collecting variables | 0.030s | |
| Time for solving dependencies | 0.001s | |
| Time for building hierarchy | 0.000s | |
| Time for building classification | 0.050s | |
| Time for exporting data | 0.005s | |
| Time for Analysis | 122.635s | |
| CPU time for analysis | 141.270s | |
| Time for analyzing result | 0.001s | |
| Total time for CPAchecker | 123.621s | |
| Total CPU time for CPAchecker | 144.150s | |
| Time for statistics | 0.054s | |
| Time for Garbage Collector | 1.302s | in 57 runs |
| Garbage Collector(s) used | G1 Old Generation, G1 Young Generation | |
| Used heap memory | 674MB ( 643 MiB) max; 323MB ( 308 MiB) avg; 693MB ( 660 MiB) peak | |
| Used non-heap memory | 54MB ( 51 MiB) max; 52MB ( 49 MiB) avg; 55MB ( 52 MiB) peak | |
| Used in G1 Old Gen pool | 163MB ( 155 MiB) max; 97MB ( 93 MiB) avg; 163MB ( 155 MiB) peak | |
| Allocated heap memory | 871MB ( 831 MiB) max; 721MB ( 688 MiB) avg | |
| Allocated non-heap memory | 57MB ( 54 MiB) max; 54MB ( 52 MiB) avg | |
| Total process virtual memory | 12222MB ( 11656 MiB) max; 12217MB ( 11651 MiB) avg |
| # | Configuration Name | Configuration Value |
|---|---|---|
| 1 | analysis.entryFunction | main |
| 2 | analysis.name | svcomp23 |
| 3 | analysis.programNames | no_context/combo2.c |
| 4 | analysis.selectAnalysisHeuristically | true |
| 5 | analysis.summaryEdges | true |
| 6 | cfa.simplifyCfa | false |
| 7 | cfa.useCFACloningForMultiThreadedPrograms | true |
| 8 | counterexample.export.compressWitness | false |
| 9 | counterexample.export.graphml | witness.graphml |
| 10 | cpa.arg.compressWitness | false |
| 11 | cpa.arg.proofWitness | witness.graphml |
| 12 | cpa.callstack.skipFunctionPointerRecursion | true |
| 13 | cpa.callstack.unsupportedFunctions | pthread_create,pthread_key_create,sin,cos,__builtin_uaddl_overflow |
| 14 | cpa.composite.aggregateBasicBlocks | false |
| 15 | cpa.predicate.memoryAllocationsAlwaysSucceed | true |
| 16 | datarace.config | svcomp23--datarace.properties |
| 17 | heuristicSelection.addressedRatio | 0.0 |
| 18 | heuristicSelection.complexLoopConfig | components/svcomp23--configselection-restart-valueAnalysis-fallbacks.properties |
| 19 | heuristicSelection.loopConfig | components/svcomp23--multipleLoopsConfig.properties |
| 20 | heuristicSelection.loopFreeConfig | components/svcomp23--configselection-restart-bmc-fallbacks.properties |
| 21 | heuristicSelection.singleLoopConfig | components/svcomp23--singleLoopConfig.properties |
| 22 | language | C |
| 23 | limits.time.cpu | 900s |
| 24 | limits.time.cpu::required | 900 |
| 25 | log.level | INFO |
| 26 | memorycleanup.config | svcomp23--memorycleanup.properties |
| 27 | memorysafety.config | svcomp23--memorysafety.properties |
| 28 | overflow.config | svcomp23--overflow.properties |
| 29 | parser.usePreprocessor | true |
| 30 | specification | /home/artjom/CPAchecker-2.2-unix/config/properties/unreach-call.prp |
| 31 | statistics.print | true |
| 32 | termination.config | svcomp23--termination.properties |
| 33 | termination.violation.witness | witness.graphml |
This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.
License: Apache 2.0 License
Source: {{dependency.repository}}
{{dependency.copyright}}
License:
Full text of license
{{dependencies.licenses[dependency.licenseId]}}